НАТУРАЛЬНЫЙ ВЫВОД
----------------------------------------------------------------------------
     Правила НАТУРАЛЬНОГО ВЫВОДА.

     Конъюнкция:
    F1   F2       F1 & F2       F1 & F2
&i  -------   &e1 -------   &e2 -------
    F1 & F2          F1            F2

     Дизъюнкция:
                                [¬F1] [¬F2]               [F1] [F2]
      F1            F2               +            F1VF2    F3   F3
Vi1 -------   Vi2 -------     Vi3 -------     Ve  ----------------
    F1 V F2       F1 V F2         F1 V F2                  F3

      Импликация:
     [F1]                                  [¬F3] [F2]
      F2          F1>F2  F1         F1>F2    F1   F3
>i  -------   >e1 ---------     >e2 ----------------
    F1 > F2          F2                     F3

      Отрицание и ложь:
                [F]       [¬F]
   ¬F   F        +          +
+i ------    ¬i ---     ¬e ---
     +          ¬F          F

      Кванторы:                                      [(Svw)F]
    (Svw)F        A.v F        (Svt)F         E.v F    F1
Ai+ ------   Ae- ------    Ei- ------     Ee+ -----------
    A.v F        (Svt)F         E.v F               F1
     Обозначения: w - константа,  не встречающаяся в заключениях Ee+ и Ai+ и
гипотезах, от которых эти заключения зависят; t - терм, свободный для v в F;
(Sxy)F - подстановка: в F заменить x на y.

----------------------------------------------------------------------------
     Правила ПОИСКА НАТУРАЛЬНОГО ВЫВОДА.

     Конъюнкция:                          Дизъюнкция:
&ai  |- F1&F2 => |-F1 / |-F2         Vai  |- F1VF2 => ¬F1;¬F2 |- +
&si  F1; F2 => F1&F2                 Vae  F1VF2 |- F3 => F1|-F3 / F2|-F3
&se1 F1&F2  =>  F1                   Vsi1 F1 => F1VF2
&se2 F1&F2  =>  F2                   Vsi2 F2 => F1VF2

     Импликация:                                  Отрицание и ложь:
>ai  |- F1>F2 => F1|-F2                      +si     ¬F; F => +
>ae2 F1>F2|-F3 => ¬F3|-F1 / F2|-F3           +del +|- F =>
>ae  F1>F2 |-F2 => |-F1                      ¬ai    |- ¬F => F |- +
>si  F2 => F1>F2                             ¬ae1  |- F => ¬F |- +
>se  F1>F2; F1 => F2                         ¬ae2 ¬F|- + => |-F

     Кванторы:
Aai+ |- A.vF => |- (Svw)F                        w - новая константа
Ase  A.vF => (Svt)F                              t - терм, свободный
Eai  |- E.vF => ¬E.vF |- (Svt)F                  для v в формуле F
Esi  F => E.v (Stv)F
Ese+ E.vF => (Svw)F
----------------------------------------------------------------------------